\documentclass{beamer}

\usepackage[portuguese]{babel}
\usepackage[latin1]{inputenc}
\usepackage{array}
\usepackage{graphicx}
\usepackage{verbatim}
\usepackage{xcolor}
\usepackage{longtable}

\usetheme{Boadilla}

\newcommand{\rotimes}{\textcolor{red}{\blacklozenge}}
\newcommand{\gotimes}{\textcolor{green}{\blacklozenge}}

\title{Modela\c{c}\~ao de um Servidor de Publicidade (AdServer) em VDM}
\author{Jo\~ao Paz \and Pedro Ara\'ujo}
\date{\today}

\begin{document}

\section{Problema Proposto}

\frame{\titlepage}

\frame{
\frametitle{Objectivos}
Os objectivos:
\begin{itemize}
 \item Modelar em VDM++ um servidor de publicidade (Ad Server)
 \item Testar o modelo
 \item Validar o modelo
\end{itemize}
}

\frame{
\frametitle{O que \'e um servidor de publicidade?}
\begin{itemize}
 \item \'E um servidor web que armazena publicidades usadas em campanhas online
 \item Entrega essas publicidades aos visitantes dos websites
\end{itemize}
\begin{center}
% use packages: array
\begin{tabular}{l}
\includegraphics[scale=0.25]{adserver.jpg}
\end{tabular}
\end{center}
}



\section{Implementa\c{c}\~ao}
\begin{frame}[fragile]
\frametitle{Tipos}


Vamos mostrar os tipos do servidor de publicidade e respectivos invariantes. Um servidor de publicidade cont\'em:

\begin{itemize}
        \item Registo de todos os clientes. Os clientes t\^em o seguinte tipo:
            \begin{verbatim}
	public ClientType = <WEBUSER> | <ADVERTISER>;

public Client :: type : ClientType
              name : seq of char;
\end{verbatim}
\end{itemize}
\end{frame}

\begin{frame}[fragile]
\frametitle{Tipos}
\begin{itemize}
        \item Registo das campanhas, juntamente com o anunciante e websites. As campanhas s\~ao t\^em o seguinte tipo:
\begin{verbatim}
	public CampaignType = <NORMAL> | <FREQ_CAP> 
	   | <ROAD_BLOCK> | <SEQ>;

public Campaign :: tipo : CampaignType
                   banners : seq of Banner
                   inicio : DateUtil`Date
                   fim : DateUtil`Date
                   freq : nat 

inv c == (c.banners <> [])  and
         (c.tipo = <FREQ_CAP> => c.freq >= 0) and
         (DateUtil`isAfter(c.fim,c.inicio));
\end{verbatim}
\end{itemize}
\end{frame}

\begin{frame}[fragile]
\frametitle{Tipos}
\begin{itemize}
	\item Registo das vizualiza\c{c}\~oes dos visitantes dos websites. Os websites t\^em o seguinte tipo:
\begin{verbatim}
public Website ::  zones : set of Zone
                 url : seq of char
    
inv w == w.zones <> {};
    
public Zone :: id : nat
               x1 : int
               y1 : int;
\end{verbatim}
\end{itemize}
\end{frame}


\begin{frame}[fragile]
\frametitle{Invariantes}
Os invariantes do servidor de publicidade s\~ao:
\begin{itemize}
 \item Todos os clientes que t\^em campanhas pertencem ao servidor;
 \item Todos os clientes que fazem pedidos pertencem ao servidor;
 \item As imagens de publicidade t\^em de pertencer a uma campanha;
 \item Uma imagem de publicidade apenas pertence a uma campanha;
 \item Para as campanhas de Frequency Capping, o n\'umero de visualiza\c{c}\~oes n\~ao excede o par\^ametro \emph{freq};
\end{itemize}
\end{frame}

\begin{frame}[fragile]
\frametitle{Invariantes}
Estes s\~ao os invariantes que adicionamos:
\begin{itemize}
 \item Cada website tem no m\'aximo uma campanha de cada anunciante;
\begin{verbatim}
forall ent1,ent2 in set campPert &
          ent1.client = ent2.client and 
              ent1.campaign <> ent2.campaign =>
                    forall web in set ent1.website & 
                        web not in set ent2.website
\end{verbatim}
 \item Dois websites t\^em zonas diferentes;
\begin{verbatim}
forall web1,web2 in set dunion { entry.website | 
    entry in set campPert } &
        web1 <> web2 => 
            ( (web1.zones inter web2.zones) = {} )
\end{verbatim}
\end{itemize}
\end{frame}

\begin{frame}[fragile]
\frametitle{Opera\c{c}\~oes}
A opera\c{c}\~ao principal do modelo tem a seguinte assinatura:
\begin{verbatim}
    public request : Client*Zone*DateUtil`Date ==> ()
\end{verbatim}
\begin{enumerate}
    \item Recolhemos a informa\c{c}\~ao da campanha (getCampanha), do banner (getBanner) e do website (getWebsite);
    \item Actualizamos da informa\c{c}\~ao das vizualiza\c{c}\~oes no servidor.
\end{enumerate}
\end{frame}


\section{Opera\c{c}\~oes}
\begin{frame}[fragile]
\frametitle{Opera\c{c}\~oes}
A opera\c{c}\~ao getCampanha que gere campanhas que est\~ao associadas ao website aonde se encontra o webuser. Tem a seguinte assinatura:
\begin{verbatim}
    private getCamp:Website*DateUtil`Date ==> Campaign
\end{verbatim}
\begin{enumerate}
    \item Reunimos todas as campahas v\'alidas, ou seja, que estejam associadas ao website;
    \item Percorremos cada campanha e, se a campanha f\^or do tipo ROAD\_BLOCK fica essa escolhida, sen\~ao \'e escolhida a campanha com menos visualiza\c{c}\~oes para se manter o equilibrio entre campanhas.
\end{enumerate}
\end{frame}


\section{Testes}
\begin{frame}
\frametitle{Testes}
Foi criada a classe Test1 com os casos de testes.\\
A cobertura dos testes realizados para a classe AdServer:
\begin{longtable}{|l|r|r|}\hline
{\bf Total} & {\bf \#Calls} & {\bf Coverage} \kill
{\bf Name} & {\bf \#Calls} & {\bf Coverage} \\ \hline\hline
\endhead
Adserver`invariantes & 44 & $\surd$ \\ \hline
Adserver`addClient & 5 & $\surd$ \\ \hline
Adserver`addCampaign & 4 & $\surd$ \\ \hline
Adserver`request & 9 & $\surd$ \\ \hline
\hline
{\bf Total Coverage} & & {\bf 100\%} \\ \hline
\end{longtable}
\end{frame}

\section{Valida\c{c}\~ao}
\begin{frame}[fragile]
\frametitle{Valida\c{c}\~ao}
Com o verificador de integridade forma geradas v\'arias propriedades. Vamos ver algumas dessas propriedades:
\begin{verbatim}
\end{verbatim}
Na classe AdServer, para a opera\c{c}\~ao request()
\begin{verbatim}
    (len (camp.banners)) in set inds (camp.banners)
\end{verbatim}
Para obter o \'ultimo elemento de uma sequ\^encia acedemos \`a posi\c{c}\~ao do tamanho da sequ\^encia. Isto s\'o n\~ao \'e poss\'ivel quando a sequ\^encia \'e vazia. Este caso \'e coberto pelo invariante do tipo Campaign.
\end{frame}


\begin{frame}[fragile]
\frametitle{Valida\c{c}\~ao}
Na classe DateUtil, para a opera\c{c}\~ao daysOfMonth() que para um dado ano e m\^es retorna o n\'umero de dias;
\begin{verbatim}
(forall year : nat, month : nat & 
 month >= 1 and month <= 12 => 
 month = (1) or  month = (2) or month = (3) or 
 month = (4) or month = (5) or month = (6) or 
 month = (7) or month = (8) or month = (9) or 
 month = (10) or month = (11) or month = (12))
\end{verbatim}
Esta propriedade \'e f\'acil de comprovar. \'E gerada porque nesta opera\c{c}\~ao existe uma instru\c{c}\~ao ``case'' e n\~ao \'e coberto o caso ``others''. 
\end{frame}

\frame{
\frametitle{Dificuldades do Projecto}
\begin{itemize}
 \item A pouca informa\c{c}\~ao sobre como utilizar as propriedades de integridade;
% \item Pouca informa\c{c}\~ao sobre o ambiente de testes do VDM;
\end{itemize}
}

\frame{
\frametitle{Conclus\~oes do Projecto}
\begin{itemize}
 \item A modela\c{c}\~ao do servidor de publicidade em Alloy foi \'util para a nossa modela\c{c}\~ao;
 \item Cobrimos as classes na sua totalidade com os testes realizados;
 \item N\~ao validamos totalmente o modelo mas elevamos o n\'ivel de confian\c{c}a no modelo atrav\'es das propriedades de integridade geradas.
\end{itemize}

}

\end{document}